Discussion:Logique intuitionniste

Déduction Naturelle

Ne serait-il pas mieux de mettre les régles de déduction naturelle dans l'article correspondant ? D'autant plus que ce dernier, est touffu, peu clair, ...

Laurent, suggére de mettre dans logique intuitionniste les motivations de Brouwer, et la nouvelle approche des mathématiques constructives.

Ce qui nous amenerait à parler des régles dans Déduction naturelle.

Marc 25 janvier 2006 à 12:44 (CET)

Je n'ai pas d'objection. Mais attendons que cet article évolue, vers plus de clarté. S'il y a redondance, on supprimera ici.

Pierre de Lyon 25 janvier 2006 à 15:34 (CET)

Ebauche?

Cet article est-il encore une ébauche? Pierre de Lyon 14 mars 2007 à 22:59 (CET)

Personne n'ayant répondu à ma question, j'y ai répondu moi-même négativement et j'ai supprimé l'entête ébauche. Pierre de Lyon 7 novembre 2007 à 11:39 (CET)

Jeu de Hex

Ai-je bien compris que les parties de ce jeu sont de longueur bornée, en fonction du damier de départ ? Auquel cas, tout est fini, et je ne vois pas comment la preuve d'existence d'une stratégie gagnante ne serait pas finalement constructive. Le fait qu'elle ne donne pas de réelle stratégie semble plutôt une question de complexité, et ça n'a pas à voir avec la logique intuitionniste. Proz (d) 20 mars 2009 à 23:51 (CET)

Tu as raison. J'ajouterais deux choses

1. On utilise le théorème de Brouwer pour démontrer l'existence d'une stratégie mixte, or dans le jeu de Hex, on ne s'intéresse qu'aux stratégies pures. Que ferait-on d'une stratégie mixte ? L'existence d'une stratégie s'appuie à mon avis plutôt sur le théorème de Zermelo sur les jeux.
2. On connait depuis Nash des versions constructives du théorème de Brouwer.

Pierre de Lyon (d) 21 mars 2009 à 08:50 (CET)

Je supprime le paragraphe en question, qui repose sur une confusion, même si la démonstration d'existence d'une stratégie gagnante pour le premier joueur décrite sur Hex (sachant que le jeu est déterminé) est bien un joli raisonnement par l'absurde (mais le jeu étant fini ...). Pour le reste j'avoue mon ignorance, je ne sais pas ce qu'est une stratégie mixte. Proz (d) 21 mars 2009 à 14:19 (CET)

Euh, je n'ai pas là de ref, mais le fait qu'il existe une démonstration non constructive qu'il y a une stratégie gagnante pour le jeu d'Hex (pour un des joueurs) est très connu (me demande si Gardner n'en parle pas dans un de ses livres). Bien sûr cela ne fait sens que si on considère un jeu infini OU (je ne sais) qu'il existe une stratégie gagnante pour tout jeu d'hex fini. --Epsilon0 ε₀ 21 mars 2009 à 16:37 (CET)

1. Une stratégie « mixte » est une stratégie qui est un combinaison de plusieurs stratégies « pures » en utilisant des probabilités.
2. D'après l'article Hex, ce jeu est fini.

Pierre de Lyon (d) 24 mars 2009 à 10:22 (CET)

Je ne vois pas pourquoi une démonstration de l'existence d'une stratégie gagnante serait nécessairement constructive dans le cas d'un jeu fini. Qui fait une confusion ? peut-être que le théorème du point fixe de Brouwer sert à autre chose que les stratégies mixtes (effacer les sources avant de regarder c'est pas malin). Peut-être que le principe du tiers exclu est utilisé en dehors du théorème de Brouwer. N'y aurait-il pas une nouvelle confusion ? Là encore effacer les sources sans les regarder n'est pas très subtil. Jean-Luc W (d) 31 mars 2009 à 12:41 (CEST)

Je ne vois pas comment on peut penser que j'ai pu écrire ce qui est au dessus sans aller lire au moins l'article Hex (fort intéressant au demeurant). Les "mystères" de la communication sur les pdd wikipédiennes, mais passons. Il m'a semblé clair qu'il y avait confusion entre des problèmes de décidabilité algorithmique et de complexité. La logique intuitionniste (le sujet de l'article !) ne dit rien en tant que telle sur la complexité. La seule référence extérieure (ce n'est sûrement pas une source de ce qui était écrit dans l'article) est disponible sur l'article Hex. Elle source bien (s'il en était besoin) qu'il s'agit de complexité et donne des détails (P-SPace complet, on est dans le cadre de la deuxième proposition d'epsilon0, un jeu fini de taille n en entrée, pour que ces choses aient un sens). Quand on ne manipule que des objets finis en nombre fini, tout est vérifiable algorithmiquement (théoriquement), le tiers-exclu se démontre intuitionnistiquement. Si on part alors de ce principe, la preuve va probablement donner un algorithme idiot qui consiste à tout simuler puis à agir en conséquence, ce qui est rapidement impraticable, mais ce n'est pas le sujet.

C' est différent pour l'exemple de l'article (dû je crois à Brouwer) : on ne peut pas décider algorithmiquement qu'un réel (calculable), est ou non rationnel, pas de tiers-exclu dans ce cas (pour les intuitionnistes). Proz (d) 2 avril 2009 à 00:58 (CEST)

En effet, des commentaires comme Auquel cas, tout est fini, et je ne vois pas comment la preuve d'existence d'une stratégie gagnante ne serait pas finalement constructive ne laisse pas penser que tu as bien lu ou bien compris l'article et ses sources. En 2009, on ne connait pas de preuve constructive de l'existence d'une stratégie gagnante. Le fait que le jeu soit fini ne change en rien cet état de fait.

Je crois que tu devrais relire ce qu'est la logique intuitionniste. Il y a une source dans l'article Théorème du point fixe de Brouwer. Ce que tu sembles ne pas comprendre, c'est la question majeure de Brouwer. Il refuse une preuve non constructive. Tu devrais lire ce qu'il raconte sur ses démonstrations topologiques. La preuve de Nash utilise deux fois le principe du tiers exclu et rend sa démonstration non constructive (rien à voir avec une question de complexité). Le jeu de Hex fait beaucoup plus sens que celui cité pour l'instant. Un lecteur aura bien du mal à comprendre pourquoi Brouwer refuse des preuves pourtant limpides comme celle présentée en exemple (qui fait passer Brouwer pour au mieux un pinailleur, au pire un abruti, ce qu'il n'était pas). Avec le jeu de Hex, on comprend pourquoi le principe du tiers exclu ne fournit qu'une réponse que très moyennement satisfaisante : un joueur ne peut rien en faire de la preuve mathématique.

Pierre de Lyon confond l'usage du théorème de Brouwer. La preuve de Nash est équivalente au théorème de Brouwer, mais n'a rien à voir avec une stratégie mixte.

Pierre de Lyon confond encore la nature de la preuve de Nash, qui n'a rien à voir avec Zermelo, mais avec le principe de la stratégie volée (une invention de Nash d'après les sources). Le tiers exclus n'est pas uniquement utilisé dans la preuve du théorème de Brouwer mais déjà dans dans l'argument de la stratégie volée. les travaux de Scarf ne change donc en rien le caractère non constructif des preuves connues.Jean-Luc W (d) 2 avril 2009 à 10:02 (CEST)

1. Puisque maintenant tu m'accordes que j'ai lu l'article, un petit effort de lecture supplémentaire et tu verras ci-dessus (message du 21 mars) que notre point de désaccord ne porte pas sur le fait qu'il s'agit d'un raisonnement par tiers exclu (par l'absurde ça revient au même).
2. La référence externe que tu avais ajouté à l'article est http://maarup.net/thomas/hex/ : le paragraphe "complexité" étudie la complexité théorique de la recherche d'une stratégie gagnante (ce qui n'a de sens que si un algorithme de recherche de stratégie en fonction d'une entrée de taille n donnée existe). Lire également la thèse en lien sur la page : p 27 "the theorem is only one of existence and makes no promise of a practical construction of the winning strategy" (ne pas oublier de lire "practical") et le chap 5 en particulier la p. 31.
3. Le fait (basique) que le tiers exclu est valide intuitionnistiquement pour le fini : tu as par exemple une citation de Kleene là : en:Law of excluded middle, une explication (avec référence à Brouwer) là : http://plato.stanford.edu/entries/logic-intuitionistic/ (article de en:Yiannis N. Moschovakis.
4. L'exemple est multi-cité sur le sujet (voir en:Law of excluded middle, qui cite entre autres en:Martin Davis). C'est un exemple pédagogique qui permet de comprendre simplement pourquoi on conteste le tiers-exclu d'un point de vue constructif.
5. Le théorème du point fixe de Brouwer : je suis arrivé sur le présent article (auquel je n'avais pas participé), par son intermédiaire. Les quelques lignes sur l'intuitionnisme sont largement des contre-sens (la note 6 en particulier). Comme c'est mineur dans l'article ça ne m'a pas paru urgent d'intervenir. L'article cité de Dubucs, est tout à fait intéressant, (pas vraiment exploité dans l'article).

Un exemple qui porte sur le fini ne peut être pertinent, les point 3 et 4 clôturent ce débat. Pour le point 5 ce n'est pas le lieu de poursuivre (et si l'échange, doit être sur ce ton, ça ne m'intéresse guère). Proz (d) 4 avril 2009 à 12:51 (CEST)

Bonjour, Je ne me suis pas plongé dans le thm de Nash ou ses généralisations ultérieures, donc je ne sais dans quel cas on se trouve :

• 1. Si le thm dit qu'on a une preuve non-constructive que pour une version finie donnée du jeu "1er joueur a une stratégie gagnante", alors on sait qu'il en existe une preuve constructive (par force brute exhaustive au pire).
  • Ceci est quelque chose qui est intéressant à mettre dans l'article, pour illuster : dans le cas fini, s'il existe 1 preuve non-constructive, il en existe une preuve constructive (et ce n'est pas vrai dans le cas d'un jeu infini.). En l'illustrant par l'exemple du jeu d'Hex qui est très connu.
• 2. Si le thm va plus loin et dit qu'on a une preuve non-constructive que pour toute version finie donnée du jeu "1er joueur a une stratégie gagnante" (ce qui me semble le cas)alors :
  • 2.1. pour tout n, il existe une preuve constructive, que "1er joueur a une stratégie gagnante" (toujours par force brute par exemple).
  • Mais on n'a pas forcément 2.2. Il existe une preuve constructive, que pour tout n, "1er joueur a une stratégie gagnante" . A moins que 2.1. --> 2.2. (cela ne me semble pas évident, mais c'est possiblement un thm classique de calculabilité, le savez-vous ?)
  • Si 2.1. n'implique pas 2.2. , là l'exemple du cas d'Hex est aussi intéressant à mettre dans l'article que le célèbre exemple : existent 2 irrationnels a et b tels que a^b est un rationnel.
• Dans tous les cas, quelque chose qui n'est pas anodin de mentionner (mais ce peut être fait rapidement), c'est que l'on peut démontrer à une époque donnée l'issue d'un jeu joué parfaitement en utilisant le tiers exclu, alors qu'à cette même date on ne peut le faire sans le tiers exclu vu la barrière combinatoire. ex : à ma connaissance pour le jeu d'échecs qui est fini (certaines règles de nullité l'impliquent) on ne sait l'issue (gain blanc, gain noir ou nulle) d'une partie parfaitement jouée des 2 côtés, ce qui fait que le thm de Nash concernant Hex est intéressant à cet égard (mais ça relève p.-e. plus de l'article sur la théorie des jeux).

Après peut bien sûr se poser une question de la complexité algorithmique (np, time, space) en fonction de la taille de l'entrée, mais là cela ne concerne pas la distinction constructif/ non-constructif.

--Epsilon0 ε₀ 2 avril 2009 à 22:10 (CEST)

D'un point de vue formel, l'énoncé est un énoncé d'arithmétique (tout se code par des entiers), le prédicat "s est une stratégie gagnante pour le jeu de taille n" est récursif (pour des raisons simples, primitif récursif par ex.). Comme il n'y a qu'un nombre fini (2 coups d'exponentielle en gros) calculable de stratégies, n étant fixé, le prédicat "le jeu de taille n admet une stratégie gagnante" est récursif également. Un tel prédicat P(n) équivaut à sa double négation (arguments développés ci-dessus en gros). La preuve se fait par l'absurde pour chaque n (on ne suppose pas que c'est le fait que pour toute taille de jeu le premier joueur n'a pas de stratégie gagnante qui mène à une contradiction) donc on a bien montré "Pour tout n P(n)" intuitionnistiquement.

De plus, même si c'était le cas, pour un énoncé P(n) décidable (donc équivalent à sa double négation), on montre facilement que "non non Pour tout n P(n)" équivaut à "Pour tout n P(n)" intuitionnistiquement. Tu montres donc que "Pour n P(n)" est prouvable en arithmétique intuitionniste ssi il l'est en arithmétique classique (on peut aller jusqu'à pour tout il existe ..., en fait mais il faut d'autres arguments).

Pour que 2.1 n'entraîne pas 2.2, il faut être dans une théorie où tu n'as pas de preuve classique non plus, tu es exactement dans des énoncés Pi^0_1 du type Gödel (th. valide intuitionnistiquement d'ailleurs), ça dépend de la théorie, et ici c'est hors de propos. Proz (d) 4 avril 2009 à 13:20 (CEST)

Proz a raison, j'ai tort. L'argument est simple : le tiers exclu est autorisé pour les ensembles finis dans la logique intuitionniste. La raison est fort bien expliquée dans en:Law of excluded middle. Jean-Luc W (d) 4 avril 2009 à 13:07 (CEST)

Merci Proz pour ces explications très claires, mon doute est totalement levé et tu as raison, comme bien souvent ;-). --Epsilon0 ε₀ 4 avril 2009 à 20:35 (CEST)

En fait, les logiciens qualifient de « décidable » un prédicat P pour lequel on peut prouver $\forall x,P(x)\vee \neg P(x)$. Ce que Proz vient de dire, c'est que tous les prédicats sur les ensembles finis sont décidables. Pierre de Lyon (d) 6 avril 2009 à 11:33 (CEST)

Je ne me mêlerai certes pas du jeu de Hex ; cependant, concernant les ensembles finis, j'ai trouvé ceci dans archive.numdam.org dans un travail consacré à Heyting:

« ….and (4) if recursion theory is interpreted classically, certain intuitionistic distinctions, but not all, have their counterpart in recursion theory, if we translate effective by recursive. A simple illustration of the fourth remark : intuitionistically, not every subset of a finite set can be proved to be decidable ; classically every subset of a finite set is recursive. » Je ne sais pas si ça a à voir avec ce que vous dites. --Michel421 (d) 1 novembre 2009 à 18:59 (CET)

Il s'agit d'ensembles d'entiers. Ca signifie me semble-t-il que l'on peut définir un sous-ensemble d'un ensemble fini (au sens intuitionniste) par des moyens non constructifs, en utilisant un prédicat non décidable : dans ce cas l'appartenance ne serait pas décidable. En fait il est faux de dire ex abrupto que le tiers exclu est autorisé pour les ensembles finis en logique intuitionniste, il faut encore que les objets eux-mêmes soient finis (pas seulement l'ensemble) ce qui est le cas dans l'exemple en cause ici (le bon argument utilise la complexité logique des prédicats en cause). Mais quand tu définis un sous-ensemble d'un ensemble fini tu peux introduire de l'infini (dans la preuve d'appartenance à ce sous-ensemble, en le faisant dépendre d'un prédicat sur les entiers qui n'est pas décidable). La notion d'ensemble et surtout de sous-ensemble utilise l'extensionnalité, or l'égalité extensionnelle n'a aucune raison d'être décidable, donc il faut être prudent avec ces notions pour l'intuitionnisme. Proz (d) 1 novembre 2009 à 20:20 (CET)

Bibliographie sur jeux et construction

Afin de bien situer de quoi on parle, il me parait intéressant de proposer une bibliographie.

Sur les jeux en général

Deux livres généraux de cours sur la théorie des jeux, où sont définis, entre autres, les concepts de stratégie mixte et d'équilibre de Nash

1. M. J. Osborne. An Introduction to Game Theory, Oxford, 2004.
2. M. J. Osborne et A. Rubinstein. A Course in Game Theory, The MIT Press, Cambridge, Massachusetts, 1994.

auquel il faut ajouter l'article de Zermelo de 1913: On an Application of Set Theory to the Theory of the Game of Chess in Rasmusen E., ed., 2001. Readings in Games and Information, Wiley-Blackwell: 79-82.

Sur la théorie algorithmique des jeux

Il s'agit d'une théorie plus récente où ce qui est mis en évidence est l'aspect algorithmique des jeux avec une focalisation sur le théorème de Brouwer constructif.

1. Contantinos Daskalakis, Paul W. Golberg et Christos H. Papadimitriou. The complexity of computing a Nash equilibrium. Communications of the ACM, 52(2):89--97, 2009. Un article tout récent qui fait une excellente synthèse du sujet par leurs initiateurs, avec une très bonne présentation du théorème de Brouwer constructif.
2. Noam Nisan, Tim Roughgarden, Eva Tardos, and Vijay V. Vazirani, Algorithmic Game Theory. Cambridge University Press, New York, NY, USA, 2007. une somme complète sur le sujet.
3. David S. Johnson, The NP-completeness column: Finding Needles in Haystacks, ACM Transactions on Algorithms, 3(2), 2007

Pierre de Lyon (d) 6 avril 2009 à 11:25 (CEST)

Intuitionnisme en théorie des ensembles

Si je suis lecteur de Wiki et que je me pose la question « étant donné E⊂X, y a-t-il un procédé de construction de l'ensemble des éléments de X qui n'appartiennent ni à E ni à C_XE ? » est-ce que l'article me fournit tous les éléments qui me permettraient de dire oui, de dire non, ou de dire pourquoi la question n'a pas de sens ?--Michel421 (d) 25 octobre 2009 à 00:04 (CEST)

Si je l'ai bien comprise, il me semble que cette question n'a pas de sens. De même qu'on ne peut pas tout démontrer en math, on ne peut pas tout mettre dans un article. --Pierre de Lyon (d) 25 octobre 2009 à 13:42 (CET)

Alors, partons sur quelque chose de plus simple: est-ce qu'en logique intuitionniste il peut arriver que E ≠ C_xC_xE ? Normalement oui, car la double négation non[non x∈E] n'entraîne pas x∈E. J'ai cependant du mal à imaginer à quoi pourrait ressembler [C_xC_xE] - E (on parle d'ensembles infinis). --Michel421 (d) 27 octobre 2009 à 09:54 (CET)

Soit P un prédicat, on dit que P est décidable si pour tout x on a P(x) ∨ non P(x). Si E est défini par un prédicat décidable alors oui E=C CE. (N.B. Je ne sais pas ce que signifie le souscrit x). Si P n'est pas décidable, il existe des x pour lesquels on ne pas dire si ils appartiennent à E ou non. On ne pourra pas démontrer « pour tout x∈X, non non P(x) ⇒ P(x) »--Pierre de Lyon (d) 28 octobre 2009 à 21:52 (CET)

Merci pour la réponse. "X" est placé en indice pour indiquer que c'est du complémentaire par rapport à X qu'il s'agit. --Michel421 (d) 29 octobre 2009 à 09:52 (CET)

Typo

Section approche formelle, je lis "si pour tout monde $m'$ tel que $m\leq m'$ on a si $m\Vdash \psi$ alors $m\Vdash \theta$.", je crois que les deux derniers m sont des m', c'est la seule chose qui a du sens, si quelqu'un peu confirmer se serait sympa, mais comme j'ai peu de doute j'édite.

--Arthur MILCHIOR (d) 7 mai 2010 à 18:25 (CEST)

Présentation de l’exclusion du tiers-exlclus

Le document commence avec une présentation des fondements de l’exclusion du tiers-exclus. Je me demande s’il n’y aurait pas une erreur dans la présentation : « Si ${\sqrt {2}}^{\sqrt {2}}$ est rationnel,  » ne devrait-il pas être « Si ${\sqrt {2}}^{\sqrt {2}}$ est irrationnel,  » ? En tous cas, ce serait nécessaire pour que ce soit cohérent avec l’énoncé. Dans tous les cas (non mathématicien), cette présentation ne me parait pas aisément compréhensible. --Hibou57 (d) 7 juin 2010 à 20:07 (CEST)

@Anne Bauval: merci pour les tentatives de rendre la motivation de l’exclusion du tiers-exclus plus claire, mais je ne la trouvais pas encore suffisamment claire. Après m’être soigneusement (enfin, du mieux que j’ai put) penché sur la question, j’ai tenté d’ajouter encore quelques éléments à la formulation. Pouvez-vous vérifier ? Merci. J’espère ne pas être trop ennuyeux avec mon insistance sur ce point, mais c’est que l’exclusion du tiers-exclus semblant si importante dans cette logique, je trouve important d’en faire un aspect compréhensible. Si mes modifications sont fausses, ce sera en tous les cas le signe que je ne l’ai pas encore compris. Merci et bonne journée.

--Hibou57 (d) 8 juin 2010 à 16:10 (CEST)

« Rappelons qu'en déduction naturelle… »

Ue phrase extraite du document : « Rappelons qu'en déduction naturelle $\Gamma \vdash \varphi$ doit se lire ... ». Mais cela n’est dit nul part auparavant, donc ce n’est pas un rappel. Manque t-il quelque chose ou faut-il re-éditer la formulation ? Dans le doute, je préfère poser la question.

--Hibou57 (d) 7 juin 2010 à 20:28 (CEST)

Les trois connecteurs

Le document contient la phrase : « est le fait que chaque connecteur ($\vee ,\wedge ,\bot$)… ». Mais $\bot$ n’est pas un connecteur, il est le symbole de la contradiction. N’y a-t-il pas confusion avec $\vdash$, qui lui est par contre effectivement utilisé comme un connecteur ? Comme je ne suis pas particulièrement spécialiste de la logique intuitionniste, j’hésite à corriger moi-même.

--Hibou57 (d) 7 juin 2010 à 20:35 (CEST)

Oui, c’est certain, il y a une erreur ici, et c’est en fait $\Rightarrow$ et non même pas $\vdash$, comme cela est confirmé par les règles d’introduction et d’élimination des connecteurs. Je corrige. Si je fait erreur avec cette modification, il n’y aura qu’à revenir en arrière, mais c’est une certitude pour moi qu’il y a une erreur.

--77.198.58.167 (d) 7 juin 2010 à 21:45 (CEST)

$\bot$, ou "bottom" ou le Faux (comme le Vrai) est un connecteur, c'est un connecteur 0-aire et d'ailleurs il se retrouve, au moins en logique classique, parmi les 4 connecteurs unaires (vrai, faux, position et négation), 16 connecteurs binaires, etc. $\vdash$ est le symbole de la déduction, il se comporte si on veut comme le connecteur qu'est l'implication, sauf qu'on n'est pas dans le langage mais dans le métalangage. --Epsilon0 ε₀ 8 juin 2010 à 11:07 (CEST)

D’accord, mais comme il ne semble pas exister de symbole explicite pour le Vrai, je pense que c’est complet. Comme personne n’a annulé la modification (c’était moi sous 77.198.58.167, je me suis trouvé déconnecté accidentellement), je pense qu’elle était juste. À moins que personne ne l’ai contrôlé (oops, je voudrais être sûr)… Merci pour le complément d’explication ; et c’est donc un connecteur 0-aire. OK.

--Hibou57 (d) 8 juin 2010 à 15:06 (CEST)

Si on a besoin d'un symbole pour le vrai on en invente un ou on utilise T, comme true et l'inverse du bottom $\bot$, ce qui est le plus usuel avec le V francophone. --Epsilon0 ε₀ 8 juin 2010 à 15:25 (CEST)

À propos des derniers ajouts

J’étais bien intéressé par ce sujet que j’avais déjà abordé à d’autres occasions sans en connaitre le nom véritable. Pourtant, j’ai décidé de ne plus éditer le sujet ici, et de le poursuivre sur un autre site. J’en donnerai les raisons un autre jour sur ma page de discussion (ça me fatigue ces problèmes que wikipédia a avec le monde extérieur, et son mépris même des sources, ça ne s’arrête pas au nofollow, c’est encore plus grave que je ne le pensais). Malgré tout, si j’ai fait des erreurs, n’hésitez pas pour autant à me le dire quand-même sur ma page de discussion.. — Le message qui précède, non signé, a été déposé par Hibou57 (discuter)

Semantique de la logique intuitioniste

Dans "aspect formel" je préfère la définition de modèle comme un triplet $<U,R,I>$ où R est un pré-ordre. J'ai donc remplacé ordre par préordre dans l'article.

Il est prouvé dans la référence "Introduction à la logique" que la validité pour les modèles pré-ordonnés est équivalente à celle des modèles ordonnés. De plus dans ce même livre, il est aussi prouvé que si la formule A a un modèle, elle a un modèle fini dont les états sont des sous-ensembles de sous-formules de A, ce qui prouve la décidabilité de la logique intuitionniste propositionnelle. Liviusbarbatus (d) 20 mai 2011 à 09:50 (CEST)

Je pense qu'il ne faut pas parler de logique modale dans la sémantique mais juste de modèle de Kripke pour les raisons suivantes ː

• ça fait beaucoup de notions à ingurgiter (on vient à peiner de définir la syntaxe et un système de preuve que l'on va déjà plonger ce langage dans un autre ː)... non, non, non)
• j'ai rajouté une sous-section plus tard où je donne la traduction en logique modale explicitement

Bientôt, je vais retravailler la section "sémantique" en ː

• donnant une explication intuitive des mondes possibles dans ce contexte (les étapes dans une démonstration)
• peut-être donner un exemple (quelqu'un en a un sous la main issu de la littérature ?)

--Fschwarzentruber (discuter) 15 avril 2016 à 01:17 (CEST)

Je suis tout-à-fait d'accord qu'il ne faut pas parler de logique modale. Outre que ça introduit un concept de plus, parler de logique modale ex abstracto n'a pas de sens, car la (une?) logique modale est une extension par une (des) modalité(s) d'une autre logique, or cette autre logique peut être classique ou intuitionniste et l'on fait alors une pétition de principe. OK pour participer à la restructuration de cette section. Quel type d'exemple désires-tu? Je veux bien en proposer un. --Pierre de Lyon (discuter) 15 avril 2016 à 11:54 (CEST)

Excellent ǃ Alors je propose d'avoir l'exemple tout simple de Semantical Analysis of Intuitionistic Logic I, Saul A. Kripke. Je vais l'ajouter là. Puis je te laisse la main sur la restructuration de la section.--Fschwarzentruber (discuter) 15 avril 2016 à 16:59 (CEST)

Je te laisse la main. On peut peut-être ajouter aussi un exemple où on voit une structure d'arbre.--Fschwarzentruber (discuter) 15 avril 2016 à 17:08 (CEST)

logique intuitionniste et logique classique

Bonjour, je ne comprends pas une phrase de l'article, peut être est ce du à mon faible niveau:

"Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste, corroborant le fait que la logique intuitionniste n'est pas une logique à part, mais fait bien partie de la Logique"

Je ne comprends pas bien le sens: Cela veut il dire qu'on peut déduire les mêmes théorèmes finalement en logique intuitionniste qu'en logique classique?

Merci.

--Nicobzz (d) 13 juillet 2011 à 05:46 (CEST)

Si on prend une formule valide de la logique classique et qu'on la transforme en saturant toutes ses sous formules et elle-même par des doubles négations (exemple : A ou non A transformée en non(non[non non A ou non non non A]) ) on obtient une formule valide de la logique intuitionniste. Pour une transformation un peu plus subtile voir la section Inclusion de la logique classique dans la logique intuitionniste. En ce sens on peut simuler la logique classique dans la logique intuitionniste et la logique classique apparaît comme un cas particulier de la logique intuitionniste ... ce qui est normal car elle a des axiomes en moins et via affirme moins, sachant que le langage est le même. --Epsilon0 ε₀ 13 juillet 2011 à 14:05 (CEST)

Donc il est possible de traduire un raisonnement par l'absurde de logique classique en logique intuitionniste ? Ou plutôt, cela signifie-t-il que pour toute démonstration par l'absurde, il existe nécessairement une démonstration qui n'utilise pas le raisonnement par l'absurde ? Dans ce thème de l'inclusion, le cas du raisonnement par l'absurde devrait être spécialement traité dans l'article. --Jean-Christophe BENOIST (d) 13 juillet 2011 à 14:14 (CEST)

Le raisonnement par l'absurde est : non(A) |- Faux, donc A, ou si on préfére |- non(non A) --> A. On ne l'a pas en logique intuitionniste pour toute formule, mais si A est non B, cela nous donne non(non (non B) --> non B qui, sauf erreur, est valide en logique intuitionniste. Donc le raisonnement par l'absurde marche en logique intuitionniste pour certaines formules, mais pour pour toutes. Et à ta question cela signifie-t-il que pour toute démonstration par l'absurde, il existe nécessairement une démonstration qui n'utilise pas le raisonnement par l'absurde ?, la réponse est non : ces 2 logiques sont bien distinctes. Mais intuitivement (si je puis me permettre) on peut côté intuitionniste voir la logique classique comme une logique peu subtile qui s'applique à des formules très particulières. --Epsilon0 ε₀ 13 juillet 2011 à 15:35 (CEST)

Oups; je m'aperçois que j'avais inversé mentalement l'ordre d'inclusion entre les deux logiques quand j'ai fait ma remarque. A ma décharge, c'est la phrase rapportée par Nico "Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste, corroborant le fait que la logique intuitionniste n'est pas une logique à part, mais fait bien partie de la Logique" qui m'a induit en erreur. Si la "logique intuitionniste fait partie de la Logique" (sous-entendu classique) alors l'ordre d'inclusion devrait être LI inclus dans LC. Mais en fait, LC est inclus sans LI. Donc la phrase citée ne me parait pas justifiée : la LI étant plus "vaste" que la LC, elle peut être tout à fait "autre" et ne "fait partie" d'aucune autre logique. --Jean-Christophe BENOIST (d) 13 juillet 2011 à 16:04 (CEST)

J'ai modifié la phrase de l'introduction en espérant que ce soit plus clair en Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste et ceci bien que l'ensemble des formules valides de la logique intuitionniste soit strictement inclus dans l'ensemble des formules valides de la logique classique. Ceci car c'est bien LI qui est incluse dans LC et non l'inverse : on passe de LI à LC en rajoutant des axiomes non déductibles des autres. Mais c'est vrai qu'alors ce codage de LC dans LI paraît très étonnant (je ne vois pas d'équivalent pour exemple dans le domaine que tu connais bien des automates/ machine de Turing). --Epsilon0 ε₀ 13 juillet 2011 à 16:22 (CEST)

voilà,c ce que je me disais je ne comprenais que LC soit inclus dans LI alors que LC a plus d axiomes. Nicobzz

Logique intuitionniste ou intuitionnisme ?

L'article s'appelle "Logique intuitionniste" et ne parle que d'elle. Donc j'aime le titre. Mais le paragraphe introductif et la section "Approche informelle" parle d'intuitionnisme. Quid de faire une introduction qui présente la logique intuitionniste et qui parle d'intuitionnisme. Puis la première section peut s'appeler "Intuitionnisme". Je n'aime pas le titre "Approche informelle"... il n'y a jamais eu d'approche informelle. C'est bizarre. En plus, la section contient des formules. J'ai même supprimé des symboles peu connus par le lecteur non connaisseur comme la négation etc. Qu'en pensez-vous ? --Fschwarzentruber (discuter) 12 avril 2016 à 19:39 (CEST)

Il est vrai que le paragraphe "approche informelle" appartient plus à intuitionnisme qu'à cet article. Et on peut en effet donner une approche "intuitive" de l'intuitionnisme.--Jean-Christophe BENOIST (discuter) 12 avril 2016 à 20:30 (CEST)

Exemples de différences avec la logique classique

La section (que j'ai déplacé dans la section "Comparaison") est bien sauf que ː

• Elle parle surtout de loi de Morgan etc. → il faut un titre plus clair. On compare ici les validités (ou les théorèmes)
• Je trouve que ça serait plus simple avec un tableau comme j'ai fait pour la section "Syntaxe" (qui manquait car ce n'était pas clair comment lire les formules de la logique intuitionniste en lisant l'article). Je vois bien un tableau avec deux colonnes. Le monde classique et le monde intuitionniste.

Qu'en pensez-vous ?--Fschwarzentruber (discuter) 12 avril 2016 à 21:26 (CEST)

La sous-section "Exemples de différences avec la logique classique" est assez complète mais confuse. Je n'ai pas encore supprimé la sous-section. Je préfère avoir votre avis. Au lieu de cela, je vous propose un tableau (placé dans la sous-section).

"Les opérations ne sont pas définies l’une par rapport à l’autre (voir plus loin), et ne sont définies qu’en elles-mêmes." => j'ai rajouté une section non-interdéfinissabilité dans "Syntaxe". C'est un point trop important ː il vaut mieux annoncer la couleur au début. " ne sont définies qu’en elles-mêmes." n'est pas très clair.

J'ai présenté la lecture intuitive dans la syntaxe (appelée "interprétation" dans l'article). Je n'aime pas trop le mot "interprétation" car cela fait penser aux modèles. Là aussi, savoir lire les formules d'une logique intuitivement, c'est hyper crucial et ça vient trop tard dans l'article.

On ne peut pas conclure que A \Leftrightarrow \lnot \lnot A est vrai. => vrai... au sens valide. La sous-section utilise trop souvent le mot "vrai" pour "prouvable".

Je trouve les exemples avec des nombres réels très confus. La logique intuitionniste ne parle pas de nombres réels. Je préfère des exemples plus "simplets".

Le découpage en sous-section est flou. Par exemple, "conjonction" ou "disjonction" parle tous les deux de "ou" et de "et".

--Fschwarzentruber (discuter) 15 avril 2016 à 00:39 (CEST)

Je ne comprends rien aux tableaux, qui n'expliquent rien et disent des choses fausses. Je serais même pour supprimer l'ensemble de la section intitulée Exemples de différences avec la logique classique sauf le premier paragraphe qui est essentiel. La différence entre la logique classique et la logique intuitionniste ne réside pas dans le fait que la première aurait à voir avec le « vrai » tandis que la seconde aurait à voir avec le « démontrable ». Il y a un système de déduction en logique classique donc une notion de démontrable. Il y a des modèles en logique intuitionniste donc une notion de validité donc de « vérité ». --Pierre de Lyon (discuter) 15 avril 2016 à 16:47 (CEST)

Nécessité

Est-ce qu'en 2016, la modalité « nécessité » ou « nécessairement » (écrite □) ne devrait pas être renommée « constructivement » ? Je trouve que nécessité fait un peu ringard. --Pierre de Lyon (discuter) 15 avril 2016 à 13:03 (CEST)

□A se lit "nécessairement A est vraie" en logique modale aléthique. J'ai l'impression que les gens disent aussi "nécessairement A est vraie" (histoire de dire quelque chose) quand l'opérateur □ est abstrait. Ici, je suis d'accord avec vous ː □ n'est pas abstrait. Dans la traduction de la logique intuitionniste en logique modale S4, □A se lit, "A est prouvable" (cf. http://plato.stanford.edu/entries/goedel/#IntProLogIntS4). Je pense qu'on devrait dire ça. J'ai placé la traduction vers la fin de l'article. Je pense que la sémantique de la logique intuitionniste peut être expliquée sans faire référence à la logique modale (par soucis de simplicité). --Fschwarzentruber (discuter) 15 avril 2016 à 13:43 (CEST)

La question du tiers-exclus

J'ai ajouté un bandeau travail inédit au paragraphe la question du tiers-exclus. Cependant, ça n'est pas seulement inédit, c'est aussi faux. Ce n'est pas la négation qui est différente en logique intuitionniste par rapport à la logique classique, ce sont tous les connecteurs et j'aurais envie de dire, tous les connecteurs sauf la négation. Je propose que ce paragraphe soit supprimé, sauf si quelqu'un souhaite le maintenir. Dans ce cas cette personne devra en améliorer la rédaction pour le rendre compréhensible et le sourcer. --Pierre de Lyon (discuter) 15 avril 2016 à 16:17 (CEST)

J'ai lu le paragraphe la question du tiers-exclus et je n'y comprends rien. Il y a trop de phrases vagues comme "après tout, des similitudes syntaxiques n’indiquent pas nécessairement des similitudes sémantiques" ou "son interprétabilité est faible.". Je préconise ː

• comme vous dîtes, la suppression de ce paragraphe (en plus l'explication du tiers-exclu est CRUCIALE et est faite dans l'introduction... il vaut mieux laisser la fin de l'article pour des choses plus spécialisées)
• améliorer éventuellement l'explication du début
• améliorer la section "Syntaxe" (la logique intuitionniste propositionnelle et la logique classique propositionnelle ont exactement la même syntaxe)
• améliorer les lectures intuitives données dans la section "Syntaxe" (je ne suis pas d'accord que la négation est la même en classique et intuitionniste car elle est définie comme une macro à partir de l'implication qui est différente... mais oui, cette macro est la même)

--Fschwarzentruber (discuter) 15 avril 2016 à 16:30 (CEST)

Modèle de Kripke

Il n'y a pas de notion de temps dans les modèles de Kripke de la logique intuitionniste. Comme il est dit c'est une modèle de mondes possibles. Je propose donc d'enlever toute référence au temps. --Pierre de Lyon (discuter) 18 avril 2016 à 10:25 (CEST)

Je cite Saul Kripke (https://www.princeton.edu/~hhalvors/restricted/kripke_intuitionism.pdf) où il y a écrit p. 98 ː

• "has been verified at the point H in time". has not been verified"
• "Now given a point in time G"
• "for an arbitrary long time without gaining any new information"

C'est une explication intuitive cependant qui aide à comprendre la sémantique je trouve et je suis assez d'accord avec Kripke. A discuter. ː) Bonne journée à toi. --Fschwarzentruber (discuter) 18 avril 2016 à 10:47 (CEST)

Oui mais Kripke écrivait il y a un demi siècle. En 2016, il a beaucoup coulé d'eau sous les ponts. C'est précisément, parce que ça ne m'aide pas à comprendre que je propose d'enlever cette référence au temps. --Pierre de Lyon (discuter) 18 avril 2016 à 10:57 (CEST)

De ce que j'en ai compris, cette relation de préordre, pour Kripke, c'est le "temps" dans le sens où, si m --> m', l'(unique) agent a fourni des efforts pour aller de m à m' et a obtenu plus d'informations. On ne peut pas perdre d'informations (si p vrai dans m, alors p vrai dans m'). Donc pour moi, ça m'aide à comprendre. Mais, là où je vous rejoins, c'est que ça peut induire en erreur d'autres personnes. Et de deux, même si Kripke est l'inventeur des modèles de Kripke, il n'a pas forcément raison et ce n'est pas forcément l'unique façon de voir ces modèles. Personnellement, je suis pour parler du temps mais sous la forme "Pour Kripke, "... "Kripke pense que..." (et la référence) afin d'être le plus impartial possible. Bonne journée.

--Fschwarzentruber (discuter) 18 avril 2016 à 14:24 (CEST)

En principe il faudrait, pour trancher ce genre de questions, se référer à une source qui présente et commente les modèles de Kripke (une source secondaire), que sur Kripke lui-même (source primaire). Plus généralement, le paragraphe "Modèle de Kripke" manque de sources (secondaires !) et de vérifiabilité, au moins sur la démarche et la manière de présenter ces modèles, ce qui est précisément l'objet de votre débat. Cordialement --Jean-Christophe BENOIST (discuter) 18 avril 2016 à 17:46 (CEST)

Je suis complétement d'accord pour rajouter des sources secondaires. Bonne journée.--Fschwarzentruber (discuter) 18 avril 2016 à 17:51 (CEST)

Le livre de Karim Nour et al Introduction à la Logique, Théorie de la démonstration (2001) dit, je cite (p. 159) ː "l'ensemble |K| (des mondes) modélisent le temps, <= l'ordre sur le temps et alpha |= A signifie que A est vraie à l'instant alpha." --Fschwarzentruber (discuter) 18 avril 2016 à 21:47 (CEST)

Je serais favorable qu'on garde la notion de temps comme une possibilité d'interprétation laissée à l'appréciation du lecteur qui trouve cela utile comme aide à sa compréhension des modèles de Kripke (c'est personnellement mon cas et j'ai la même référence que ci-dessus), sans que cela soit pour autant indispensable. Theon (discuter) 19 avril 2016 à 17:12 (CEST)

Personnellement, je comprends mieux aussi avec le temps. Et c'est même du temps branché (c'est à dire qu'il y a plusieurs futurs possibles selon comment l'agent fournit l'effort pour "apprendre de nouvelles informations". Mais je comprends Pierre Lescanne et wikipedia ne doit pas prendre parti ː s'il existe des références où le temps n'est pas mentionné, on peut aussi le mentionner.--Fschwarzentruber (discuter) 19 avril 2016 à 18:17 (CEST)

Il pleut ou il ne pleut pas.

Je pense que la phrase « il pleut ou il ne pleut pas » est désastreuse comme exemple, d'autant plus qu'elle figure au tout début de l'article. En effet, elle est décidable. N'importe qui de sensé qui se promène pourra répondre « Oui il pleut » ou « Non il ne pleut pas ». Donc le tiers exclu peut être appliqué à une telle proposition. En revanche une phrase comme « Omar m'a tuer ou Omar ne m'a pas tuer » ou « Christian Ranucci a tué Marie-Dolorès Rambla ou Christian Ranucci n'a pas tué Marie-Dolorès Rambla » sont certes plus polémiques, mais ne sont pas décidables et seraient des exemples plus convaincants. L'intime conviction n'est pas la décision. --Pierre de Lyon (discuter) 11 mai 2016 à 12:21 (CEST)

On peut trouver un phrase plus anodine Dan Cole a marqué un essai ou Dan Cole n'a pas marqué d'essai. --Pierre de Lyon (discuter) 11 mai 2016 à 12:25 (CEST)

Je suis favorable pour le remplacement de l'exemple. --Fschwarzentruber (discuter) 11 mai 2016 à 12:35 (CEST)

Moi aussi, mais je me pose des questions. Je me demande si la faiblesse de ces exemples ne vient pas du fait qu'il s'agit d'un événement individuel, unique, qui peut être - plus ou moins aisément, mais ce n'est pas fondamental - falsifiable/vérifiable. "Omar m'a tuer" ne me semble pas fondamentalement différent de "il peut ou pas", ce n'est qu'une question de difficulté de vérification. Un bon exemple d'énoncé qui peut être indécidable serait-il pas plutôt "le soleil se lève tous les jours", qui référence un nombre infini d'événements ? L'indécidabilité ne concerne-t-il pas toujours, directement ou indirectement, une classe infinie d'objets ? L'indécidabilité du problème de l'arrêt, de P=NP etc.. sont tout à fait de ce genre. Même l'indécidabilité de l'axiome du choix concerne un ensemble infini d'ensembles non vides. --Jean-Christophe BENOIST (discuter) 11 mai 2016 à 13:16 (CEST)

C'est aussi mon point de vue, que l'indécidabilité concerne seulement des exemples mathématiques. J'ai cité des exemples liés à la décision d'un juge ou d'un arbitre, pour respecter le désir de l'auteur de cette phrase de donner un exemple de la vie courante (peut-être une fausse vie courante ). --Pierre de Lyon (discuter) 11 mai 2016 à 13:58 (CEST)

Pour construire l'exemple, il nous faut une conjecture non prouvée C. "C ou non C" fait office d'exemple.

* Ainsi, C = "il pleut" est un peu tiré par les cheveux car il faut que la personne n'est pas regardé par la fenêtre... (bref, l'exemple n'est pas convaincant du tout).

* Je pense qu'un exemple juridique n'est pas si mal. Si une affaire juridique C, comme C = "Christian Ranucci n'a pas tué Marie-Dolorès Rambla" n'est pas élucidée, alors C n'est pas prouvable jusqu'alors, "non C" non plus. Du coup, "C ou non C" fait office d'exemple.

* Dans une version antérieure, il y avait l'exemple ""Il existe des nombres irrationnels a et b, tels que a^b est un nombre rationnel"". Il repose sur le tiers-exclu "sqrt 2 ^{sqrt 2}" rationnel ou sqrt 2 ^{sqrt 2}" irrationnel". Mais l'humanité a démontré que "sqrt 2 ^{sqrt 2}" irrationnel" donc l'exemple n'est pas génial.

* Mais :), http://plato.stanford.edu/entries/logic-intuitionistic/#RejTerNonDat donne l'exemple C = "il existe une infinité de nombres premiers jumeaux". Qu'en pensez-vous ?

--Fschwarzentruber (discuter) 11 mai 2016 à 14:16 (CEST)

Mathématique, sourçable, c'est tout bon. Ou la conjecture de Syracuse ? mais on n'a pas répondu à mon interrogation si l'indécidabilité concerne toujours des classes infinies d'objets. C'est le cas pour C envisagé en tout cas. --Jean-Christophe BENOIST (discuter) 11 mai 2016 à 14:55 (CEST)

OK pour la conjecture des nombres jumeaux ou pour celle de Syracuse. D'autre part, (en agitant les mains) si l'égalité sur un ensemble satisfait le tiers-exclus, alors la dite égalité est décidable ; or les ensembles finis sont décidables, donc pour qu'il n'y ait pas de tiers exclus, il faut que les ensembles soient infinis. Voir par exemple le Coq'art page 286.--Pierre de Lyon (discuter) 12 mai 2016 à 14:53 (CEST)

Merci pour la réponse, il me semblait bien. Cordialement --Jean-Christophe BENOIST (discuter) 12 mai 2016 à 16:04 (CEST)

« il pleut ou il ne pleut pas » est essentiellement indécidable car prouver cela c'est (formellement) : déterminer en toute circonstance s'il peut ou non. Rien n'est décidable si les objets dont il est question n'ont pas un caractère inductif. Pas de définition inductive de la pluie ; donc, pas de preuve possible.   <STyx @ (en long break)

Section "histoire"

Le 3ème § de la section histoire ("Elle a été ensuite formalisée, sous le nom de logique intuitionniste") est mal rédigé:

• Il y a un "Godel et Kolmogorov." qui n'est relié à rien; je présume que l'auteur voulait dire "Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko et Arend Heyting ainsi que Kurt Gödel et Andreï Kolmogorov." (ces 2 sus-mentionnés ne sont pas des élèves de Brouwer).
• La section sur l'implication matérielle serait sans doute mieux à une autre place (peut-être après le 1er § de cette section).

--Duboismathieu gaas (discuter) 31 décembre 2017 à 00:06 (CET)

vu par Theon   <STyx @ (en long break) 8 janvier 2018 à 18:12 (CET)

Logique minimale

 STyx : Vous avez fait une correction avec le commentaire « La logique implicative "minimale" : non-sens : c'est aussi stupide que de parler de serpent tétraplégique ». Vous avez ajouté un lien en anglais qui n'est pas la traduction de ce qui est écrit en français. Pourriez-vous nous expliquer votre point de vue sur la page de discussion ? --Pierre de Lyon (discuter) 10 janvier 2018 à 18:27 (CET)

• "minimal" c'est un terme (trop) vague. Si on entend par là "langage minimal", alors "implicatif minimal" est un pléonasme (mais bon, c'est le même problème que pour le mot "fonction" : on en vient à parler de "fonction partiel" parce que le mot "fonction" est trop souvent (toujours! en informatique) employer pour désigner une '"application"); si l'on comprend "sans l'exfalso" alors voici une excellente analogie : logique = animal, ⊥ = pattes, donc implicatif=sans patte ; exfalso =l'usage des pattes, donc : minimal=tetraplegique.
• euh ! tu veux dire  : Vous avez ajouté un lien en anglais qui serait la traduction de ce qui n'est écrit pas en français : logique implicative.   <STyx @ (en long break) 11 janvier 2018 à 15:13 (CET)

Dans Introduction à la logique - Théorie de la démonstration, de Nour, et al., ils mentionnent bien la logique minimale p. 147. Je propose de ne pas supprimer brutalement la mention "logique minimale", mais de dire "Certains auteurs (ref à Nour et al.), ça s'appelle "logique minimale", puis "pour d'autres auteurs (mettre une ref), elle est appelée logique implicative". Bonne soirée. Fschwarzentruber (discuter) 11 janvier 2018 à 18:11 (CET)

D'accord avec logique minimale ! ... mais pas avant d'avoir introduit ⊥ sinon cela n'a pas de sens .   <STyx @ (en long break) 11 janvier 2018 à 19:24 (CET)

Audit

L'article est mal structuré ! La partie contructive (i.e. la correspondance de Curry-Howard) n'est pas exposée ! Vue la complexité du sujet une section "Introduction" (un résumé introductif comme dans tout article ou livre scientifique). Cela permettrait de mettre en évidence l'essentielle de la section. Par exemple : « Les Logique intuitionniste#Modèles de Kripke fournissent un moyen infaillible de démontrer qu'une proposition n'est pas démontrable ». Cela permettrait aussi de replacer ce que j'ai mis en commentaire ... avec des liens interne cette fois.

• Logique intuitionniste#Syntaxe du langage de la logique intuitionniste ne parle nullement de syntaxe ; mais de sémantique. !
• Logique intuitionniste#Non-interdéfinabilité des opérateurs à supprimer : c'est vague, mal dit, et fait doublon (voire "triplon" :) ) avec le reste
• Logique intuitionniste#Traduction en logique modale classique a plus sa place dans Logique intuitionniste#Sémantique de la logique intuitionniste
• Logique intuitionniste#Inclusion de la logique classique dans la logique intuitionniste : je préfère "non-non-traduction" ... mais bon
• Logique intuitionniste#Exemples de différences avec la logique classique : pfff! des tonnes ... et cela fait doublon ! ... pourquoi pas une simple liste de tautologies indécidables

A rajouter

• Théorème de Glivenko
• Heyting
• « Notons à ce propos qu'il existe, entre la logique intuitionniste et la logique classique, une infinité de logiques intermédiaires, plus fortes que la logique intuitionniste et plus faibles que la logique classique. » : à développer !
• Il faudrait également formuler (plus clairement que moi) des choses comme « pierce, tiers-exclu, ¬¬P→P, ..., ($((p\Rightarrow q)\Rightarrow r)\Rightarrow ((q\Rightarrow p)\Rightarrow r)\Rightarrow r$, einstein : (P→Q)∨(Q→P) ??) sont equivalentes/interchangeables »

etc.   <STyx @ (en long break) 11 janvier 2018 à 18:57 (CET)

D'accord à peu près avec tout. Mais la section Syntaxe présente bien la syntaxe, c'est-à-dire les constructions du langage et comment on les lit à haute voix en français. La sémantique est donnée dans la section "Sémantique". Fschwarzentruber (discuter) 11 janvier 2018 à 19:02 (CET)

le "Syntaxe du" est superflu (la syntaxe traite, à mon sens, de l'agencement des symboles) ... et le tableau donne "le sens de ..." (donc sémantique) et se contente de remplacer "vrai" par "prouvable" ... Enfin, il y a Logique intuitionniste#Relations avec la logique classique ou l'on compare encore abondamment les deux logiques.   <STyx @ (en long break) 11 janvier 2018 à 19:18 (CET)

Quelques validités

Je propose de supprimer la section « Quelques validités » à laquelle je ne comprends rien. --Pierre de Lyon (discuter) 22 mars 2019 à 09:26 (CET)

Je ne suis pas emballé par les explications de cette section. Par contre, il me paraît utile de garder la liste des exemples de la première colonne, qui permet d'illustrer la différence entre logique classique et intuitionniste. Il conviendrait alors de voir quelle forme prendraient les deux colonnes de droite : les conserver en reformulant certaines explications ? les supprimer en les remplaçant par un commentaire ? Theon (discuter) 23 mars 2019 à 07:58 (CET)

Le tableau, que j'ai mis du temps à comprendre, explique, ou tente d'expliquer, pourquoi

• quand dans la colonne 1 on a une formule de la forme A <==> B, A ==> B marche (colonne 2) et B ==> A marche (colonne 3).
• quand dans la colonne 1 on a une formule de la forme A ==> B, A ==> B marche (colonne 2) et B ==> A ne marche pas (colonne 3) … alors qu'il marche en logique classique.

Bref je trouve que ce tableau est une bonne idée mais manque de présentation et pêche un peu par ses explications. Qu'on le garde en l'améliorant ou pas, le point le plus important, me semble t-il, est de marquer les validités classiques qui ne sont pas intuitionnistes, soient, en creux dans ce tableau :

• $\lnot \lnot A\Rightarrow A$
• $\lnot (A\land B)\Rightarrow (\lnot A)\lor (\lnot B)$
• $(A\Rightarrow B)\Rightarrow ((\lnot A)\lor B)$ <-- En passant, je ne savais pas que ce n'était pas intuitionniste. Pouvez-vous confirmer ?
• $\lnot (\forall xA(x))\Rightarrow \exists x(\lnot A(x))$

--Epsilon0 ε₀ 24 mars 2019 à 00:34 (CET)

 Epsilon0 : c'est immédiat, on obtient (EM) en prenant A=B ;)   <STyx @ (en vadrouille) 24 mars 2019 à 04:47 (CET) Oui ;-) merci. (EM = excluded middle) --Epsilon0 ε₀ 24 mars 2019 à 11:45 (CET)

• Je suis pour un tableau ... mais pas celui-là. $\vdash A\Rightarrow B$ est une relation ordre $A\geq B$ entre formules closes. On n'a plus 2 classes d'equ. (comme en logique classique) ni 3 ... mais une infinité ! Ce qui m'interresse ; ce serait de faire une ébauche de cette hiérarchie (notamment ⊥>(EM)=(Pierce)=(NNPP)>(weak excluded middle)> etc. >⊤= etc.). cf. en:Intermediate logic
• appeler "explication" une reformulation de l'énoncé, quelle foutaise ! Je propose un fichier coq pour ce qui est prouvable directement (ie. sans M. de Kripke) et des colonnes pour la désignation/lien, valeur de Heyting.

Voilà un extrait d'une de mes vieilleries   <STyx @ (en vadrouille) 24 mars 2019 à 04:47 (CET)

(*
-  1: [ P \/ ~ P ]  (EM)=(E3)
-  2: [ ~~P -> P ]  (NNPP)
-  3: [ (~P -> P) -> P ]
-  4: [ (~Q -> ~P) -> (P -> Q) ]
-  5: [ ((P -> Q) -> P) -> P ]  (Pierce)
-  6: [ ~~(P \/ ~ P) ]
-  7: [ (P -> Q) -> ( Q \/ ~P ) ]
-  8: [ ~~(P \/ ~ P) -> (P \/ ~P) ]
-  9: [ ~ P \/ ~~P ] (EM ~P) (weak excluded middle) (principle of testability) (Jankov logic (KC))
- 10: [ (~Q -> P) -> (Q -> P) -> P ]
- 11: [ (~Q -> P) -> (~~Q -> P) -> P ]
- 12: [ ~~(~~P -> P) ]
- 13: [ (P -> Q) \/ (Q -> P) ]  (Einstein) (Gödel–Dummett)
- 14: [ (~Q ↔ P) -> (Q ↔ ~P) ]
- 15: [ ( ( (((P->Q) -> P) -> P) -> R ) -> ((P->Q) -> P) -> P ) -> ((P->Q) -> P) -> P  ]  (Pierce Pierce)
- 16: [ ((P->Q) -> R) -> ((Q->P) -> R)  -> R ]
- 17: [ P \/ ~ P \/ (P <-> forall Q:Prop, Q \/ ~ Q) ] (E4)
- 18: [ (~~ (~~P -> P)) ->  ~~P -> P ] (NNPP NNPP)
- 19: [(~P->Q)->(~Q->P)] undecidable
- 20: [~(P/\Q)->(~P\/~Q)] undecidable
- 21: [P->~P->Q] true
- 22: [ ((~P -> Q) -> ~P) -> ~P ]  (Pierce ~)
- 23: [ ((~~P -> P) -> (P\/~P)) -> (~P\/~~P) ]  (Scott axiom)
- 24: [ (~P -> (Q\/R)) -> ((~P->Q)\/(~P->R)) ]  (Kreisel-Putnam axiom)
- 25: [ (~Q -> P) -> ((P->Q)->P)->P ]  (Smetanich axiom)
- 26  [ (P -> Q) -> (~P \/ Q) ]

Equivalences établies :
 - true:  6 == 12 == 21 == 22 (démontrables en logique intuitionniste)
   (note (theorem de Glivenko) : toute tautologie classique de la forme [~F] est démontrable en log. int.)
 - undecidable: 1 == 2 == 3 == 4 == 5 == 7 == 8 == 10 == 14 == 18 == 26 (valeur de Heyting 1/2)
 - undecidable : 13 == 16
 - undecidable: 9 == 11  (valeur de Heyting 1)
 - 1-> 13 -> 9
 - 5 -> 15
 - 17 -> 9
*)

• Je viens de découvrir coq online ;)) ! Pour de vrais explications, il suffit de tester ... par exemple ceci :   <STyx @ (en vadrouille) 24 mars 2019 à 16:43 (CET)

NNPP → excluded_middle

Require Import Coq.Unicode.Utf8.
Definition excluded_middle : Prop := ∀ P:Prop, P ∨ ¬ P.
(** [¬¬]-elimination ([NNPP]) *)
Definition NNPP:Prop := ∀ P:Prop, ¬¬P → P.

(** preuve initiale (human style) *)
Lemma NNPP_em__ :  NNPP → excluded_middle.
Proof.
unfold NNPP.
intros NNPP P.
assert( H: (¬¬(P ∨ ¬P) → (P ∨ ¬P)) →  (P ∨ ¬P) ).
intro HP. apply HP. intro NPP.
assert ( H': ¬P → ¬¬¬P ).
intros NP NNP. apply NNP. exact NP.
apply H'. clear H'.
intros P_. apply NPP. apply or_introl. exact P_.
intro NP. apply NPP. apply or_intror. exact NP.
apply H. apply NNPP.
Qed.
(** On obtient un terme (utiliser [Print NNPP_em__.]) assez immonde, 
du au fait que l'on raisonne naturellement "des hypothèses au but" 
à l'aide de lemmes intermédaires (tactique [assert]).
Après suppression des [let], remise en ordre (béta-reduction), et omission des types ; 
cela donne : *)
Definition NNPP_em_ :  NNPP → excluded_middle :=
fun NNPP P => NNPP (P ∨ ¬P) (fun NEM => (NEM (or_intror (fun P_ => NEM (or_introl P_))))).
(** ... qui est le resultat de la preuve finale (coq (/CoC) style) suivante : *)
Lemma NNPP_em :  NNPP → excluded_middle.
Proof. unfold NNPP. intros NNPP P. apply NNPP. intro NEM. apply NEM. right. intro P_. apply NEM. left. exact P_. Qed.
(** donc, si l'on admet que [excluded_middle] n'est pas démontrable, [NNPP] ne l'est pas non plus *)

 

La constante d'Euler Mascheroni

 Remsirems : Pour décider de la rationalité de la constante d'Euler Mascheroni, il faut ou bien une démonstration constructive de sa rationalité, ou bien une démonstration constructive de son irrationalité. Il faudrait reformuler l’introduction dans ce sens, si vous le souhaitez. Pour l’instant la formulation actuelle est préférable. --Pierre de Lyon (discuter) 30 juin 2019 à 12:23 (CEST)

 PIerre.Lescanne : Je ne suis pas sûr de comprendre votre point de vue. Le problème de la formulation actuelle n'est pas qu'elle manque de clarté; c'est qu'elle est fausse! En effet, affirmer qu'il n'est pas démontrable (constructivement s'entend) que « la constante d'Euler-Mascheroni est rationnelle ou la constante d'E.-M. est irrationnelle », c'est affirmer qu'il n'existe pas, dans l'absolu, ni de démonstration qu'elle soit rationnelle, ni de démonstration qu'elle soit irrationnelle. Or tout ce que nous savons, c'est que, à l'heure actuelle, nous n'avons trouvé de démonstration ni dans un sens ni dans l'autre: mais nous n'avons aucune preuve que nous ne pourrons jamais en trouver…!

Ce qui est vrai, c'est que pour une proposition générique $P$, on ne peut pas montrer en logique intuitionniste la proposition $(P\ {\text{ou}}\ \neg P)$. Mais la phrase précédente est un théorème, et pas juste une conséquence directe des règles de l'intuitionnisme: j'entends par là qu'il y a une preuve (pas facile au demeurant) qu'aucun raisonnement intuitionniste ne permettra de conclure à $(P\ {\text{ou}}\ \neg P)$…

Cependant, lorsqu'on considère une proposition $P$ fixée (disons, « $1+1=2$ », il se peut très bien que $(P\ {\text{ou}}\ \neg P)$ soit prouvable (en l'occurrence c'est le cas, puisqu'on a une preuve de $P$. Dans le cas de la constante d'E.-M., on ne sait pas si notre ignorance sur la rationalité ou non de $\gamma$ provient de ce que c'est un indécidable (autrement dit, on n'a pas trouvé de preuve parce qu'il n'y en existe pas) ou de ce qu'on n'a simplement pas encore assez bien cherché…

La formulation de l'introduction actuelle pourrait être valide si on remplaçait la rationalité de la constante d'E.-M. par une affirmation connue pour être indécidable. Le problème, c'est que les indécidables de la logique classique ne sont pas nécessairement indécidables en logique intuitionniste, de sorte que je n'ai aucun exemple à proposer…

Au vu de ce qui précède, je vous recommande donc de ré-intégrer mes modifications, quitte à les amender sous une forme que vous trouviez plus claire. Mais en tout état de cause, on ne peut pas laisser une affirmation fausse sur WP au motif qu'elle serait plus facile à comprendre qu'une affirmation erronée…

Cordialement, Remsirems (discuter) 30 juin 2019 à 16:31 (CEST)

Je pense qu'il faut une source. Gilles Dowek donne l'exemple "le général a tué le chauffeur ou le général n'a pas tué le chauffeur" p. 81 dans Gilles Dowek - la logique, aux éditions Poche - Le Pommier!. Y-a-t-il une source pour l'exemple de la constante d'E.-M ? Merci et bonne soirée. Fschwarzentruber (discuter) 30 juin 2019 à 21:14 (CEST)

Vous dites « Ce qui est vrai, c'est que pour une proposition générique P, on ne peut pas montrer en logique intuitionniste la proposition ( P ou ¬ P ). Mais la phrase précédente est un théorème, et pas juste une conséquence directe des règles de l'intuitionnisme: j'entends par là qu'il y a une preuve (pas facile au demeurant) qu'aucun raisonnement intuitionniste ne permettra de conclure à ( P ou ¬ P )… » ; Pourriez-vous être plus précis, je ne comprends pas ce que vous voulez dire. Plus précisément qu'entendez-vous par

• phrase précédente
• pas facile au demeurant.

--Pierre de Lyon (discuter) 30 juin 2019 à 21:51 (CEST)

Pierre de Lyon. « Phrase précédente » désignait l'affirmation suivante: « Pour $P$ une proposition dont on ne sait rien, si ce n'est que c'est une proposition, il n'existe pas de preuve en logique intuitionniste de $(P\ {\text{ou}}\ \neg P)$ ».

Il est important de réaliser que l'inexistence affirmée par la phrase ci-dessous n'est pas facile à montrer! En effet, le simple fait qu'on n'ait pas le droit d'utiliser l'axiome « $P\ {\text{ou}}\ \neg P$ » en tant que règle de la logique n'exclut pas, à priori, qu'on puisse quand même le démontrer par le biais d'un raisonnement plus compliqué! Il se trouve cependant que, dans le cas d'une proposition $P$ générique, il est bel et bien exact qu'aucun raisonnement de logique intuitionniste, aussi alambiqué soit-il, ne permettra jamais de montrer $(P\ {\text{ou}}\ \neg P)$. Mais la preuve de cette affirmation est trop compliquée pour être donnée dans ces quelques lignes…

Maintenant, si on considère une proposition $P$ particulière, comme « la constante d'E.-M. est rationnelle », il y a à priori plusieurs cas possibles:

• On sait prouver (en logique intuitionniste) $P$, ou on sait prouver $\neg P$, et donc on sait prouver $(P\ {\text{ou}}\ \neg P)$;
• On sait qu'il existe une preuve en logique intuitionniste de $(P\ {\text{ou}}\ \neg P)$, mais on ne connait néanmoins pas, à l'heure actuelle, cette preuve (ce cas est paradoxal, mais il se produit, par exemple, si $P$ est l'affirmation « le $10^{10^{10}}$-ième chiffre de $\pi$ est un ‘7’ » : dans ce cas, un calcul suffisamment long permettra de savoir quel est le chiffre en question et donc d'avoir une preuve intuitionniste, soit de $P$, soit de $\neg P$ ; mais personne n'a jamais mené à bien ce calcul qui est bien au-delà de nos moyens actuels.
• On ignore, à l'heure actuelle, si la proposition $(P\ {\text{ou}}\ \neg P)$ est prouvable en logique intuitionniste ou non (c'est la situation, autant que je sache, concernant la rationalité de la constante d'Euler-Mascheroni);
• On a une preuve qu'aucun raisonnement de logique intuitionniste de permettre jamais de conclure à $P$ ni à $\neg P$, et donc (il se trouve que c'est équivalent en logique intuitionniste) qu'aucun raisonnement de logique intuitionniste ne permettra jamais de montrer $(P\ {\text{ou}}\ \neg P)$;
• Non seulement on est dans le cas précédent, mais en plus, notre preuve est valide dans le cadre de la logique intuitionniste : ce qui signifie alors qu'on dispose d'une preuve, en logique intuitionniste, de $\neg (P\ {\text{ou}}\ \neg P)$. (Attention, je ne suis pas 100 % sûr de moi sur ce dernier item).

Idéalement, il faudrait remplacer la rationalité de la constante d'E.-M. par une proposition rentrant dans un des deux derniers cas ci-dessous. Mais je pense que l'introduction y perdrait en clarté… Il me semble donc plus pertinent d'écrire quelque chose comme « alors qu'il est trivial, pour la logique classique, que l'affirmation “γ est rationnelle ou γ est irrationnelle” est correcte, en logique intuitionniste au contraire, il est tout à fait envisageable qu'une telle proposition soit fausse ! (et de fait, à l'heure de 2013, on ne connait en tout cas aucune preuve intuitionniste de “γ est rationnelle ou γ est irrationnelle“) ».

Cordialement, Remsirems (discuter) 30 juin 2019 à 22:54 (CEST)

Tout d'abord, en logique intuitionniste, on sait (c'est assez facile à (méta)démontrer une fois que l’on a la correction de la logique par les modèles de Kripke) que P ∨ ¬P n'est pas un théorème, ou dit autrement, qu'il n'y a pas de démonstration de P ∨ ¬P. En effet, il y a un modèle de Kripke qui ne valide pas P ∨ ¬P.

Il me semble que vous ne connaissez pas un point fondamental de la logique intuitionniste concernant le connecteur ∨. En logique intuitionniste, pour que l'on ait une démonstration de P ∨ Q, il faut que l’on ait une démonstration de P ou que l’on ait une démonstration de Q. Si nous appliquons cela à la proposition REM qui signifie que la constante Euler-Mascheroni est rationnelle et à sa négation, pour avoir une démonstration de REM ∨ ¬ERM, il faut que l'on ait ou bien démonstration de REM ou bien une démonstration de ¬ERM, or le 3 juillet 2019, nous n'avons aucune de ces deux démonstrations. Donc nous n'avons pas de démonstration de ERM ∨¬ERM. --Pierre de Lyon (discuter) 3 juillet 2019 à 08:47 (CEST)

 PIerre.Lescanne : En effet, je ne suis pas expert du domaine… Mon point principal était simplement de souligner que l'affirmation « la rationalité de la constante d'Euler-Mascheroni n'est pas démontrable en logique intuitionniste » n'est pas un résultat des mathématiques d'aujourd'hui et ne pouvait donc pas figurer dans l'introduction d'une page Wikipédia. La nouvelle version de la page, en revanche, règle ce souci de façon parfaitement satisfaisante. Merci donc pour votre aide ! :-) Cordialement, Remsirems (discuter) 3 juillet 2019 à 18:09 (CEST)

Prouvable et contradictoire

Bonjour,

je voudrait soulever ce qui me semble une erreur et qui amène à des difficulté de compréhension voir à des contres sens :

Il est écrit dans le paragraphe Syntaxe du langage de la logique intuitionniste > Syntaxe de la logique intuitionniste propositionnelle, dans le tableau que "A est prouvable" alors que "non-A est contradictoire". Cela me pose un problème, car il n'est pas évident (voir faux) que "être-contradictoire" est la négation d'"être prouvable". Aussi bien que qu'un énoncé qui n'est pas prouvable n'est pas nécessairement une contradiction, inversement, une proposition non-contradictoire n'est pas nécessairement prouvable. Le problème que je soulève n'est pas à proprement parler un problème de logique intuitionniste mais plutôt un problème de sémantique : Sur l'équivalence et les lien qu'entretiennent les mots "prouvable" et "contradictoire". D'autant plus, que l'on passe par simple négation, d'un mot se référant à une possibilité "prouvABLE" à un mot se référant à une particularité "contradictoire" (contredisable s'il se référait à une possibilité).

Je ne sais pas si c'est une simple erreur de traduction de texte universitaire (ou de livre sur le sujet) ou bien qu'il s'agisse d'une erreur de compréhension, ou enfin qu'il s'agit d'une erreur dans la théorie intuitionniste.

Quoiqu'il en soit, je pense que cela mérite un éclaircissement, et si jamais une correction.

Cordialement Sptc Fa — Le message qui précède, non signé, a été déposé par Sptc Fa (discuter), le 7 août 2020 à 16:28 (CEST)

Une petite correction d'abord : non-A signifie que "A est contradictoire" (et non pas que non-A est contradictoire). Sur le fond de ta question, elle reflète parfaitement la différence entre logique classique et logique intuitionniste, et tu l'as en fait parfaitement saisie. Ainsi, tu dis que « Aussi bien que qu'un énoncé qui n'est pas prouvable n'est pas nécessairement une contradiction, inversement, une proposition non-contradictoire n'est pas nécessairement prouvable ». L'article, quant à lui, dit dans la partie du tiers exclu, que « (A ou non-A) est un théorème de la logique classique, mais pas de la logique intuitionniste. Dans cette dernière, elle signifierait que nous pouvons prouver A ou prouver non-A (i.e. prouver A ou prouver que A est contradictoire), ce qui n'est pas toujours possible ». Ainsi, en logique intuitionniste, le fait que A soit non-contradictoire ne suffit pas à pouvoir le prouver, et le fait que A ne soit pas prouvable ne suffit pas à justifier que A conduit à une contradiction, ce qui correspond bien à ce que tu dis. L'alternative ou bien A est prouvable, ou bien A est contradictoire, n'est pas vérifiée en logique intuitionniste. Theon (discuter) 8 août 2020 à 07:43 (CEST)